-----------------------------------------------------------------------------
--
-- Module      :  Data.TypeLevel.Peano
-- Copyright   :
-- License     :  AllRightsReserved
--
-- Maintainer  :  eduard.sergeev@gmail.com
-- Stability   :  Highly Experimental
-- Portability :
--
-- Type-level peano numbers
--
-----------------------------------------------------------------------------

{-# LANGUAGE NoImplicitPrelude, TypeOperators, TypeFamilies, UndecidableInstances, ScopedTypeVariables #-}

module Data.TypeLevel.Peano (

   (:==:),
   (:/=:),

   (:<=:),
   (:<:),

   Zero,
   Succ,
   One,
   Two,
   Three,
   Four,

) where

import Prelude (Show(show), (+))
import Data.TypeLevel.Class
import Data.TypeLevel.Families
import Data.TypeLevel.Boolean 


data Zero
data Succ a


type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three

-- * Type-level "Eq" implementation
type instance Zero :==: Zero = True
type instance Succ l :==: Zero = False
type instance Zero :==: Succ r = False
type instance Succ l :==: Succ r = l :==: r

type instance a :/=: b = Not (a :==: b)


-- * Type-level "Ord" implementation
-- | LessOrEqual
type instance Zero :<=: Succ r = True
type instance Zero :<=: Zero = True
type instance Succ l :<=: Zero = False
type instance Succ l :<=: Succ r = l :<=: r

type instance l :<: r = (l :<=: r) :*: (l :/=: r)



-- * Type-level "Num" implementation
-- | Addition
type instance Zero :+: b = b
type instance Succ a :+: b = a :+: Succ b

-- | Multiplication
type instance Zero :*: b = Zero
type instance Succ a :*: b = b :+: a :*: b



-- * Instances

instance Numerable Zero where
    toNumber _ = 0

instance (Numerable p) => Numerable (Succ p) where
    toNumber _ = 1 + toNumber (typeValue :: p)


instance Show Zero where
    show _ = "0"

instance (Numerable p) => Show (Succ p) where
    show p = show (toNumber p)
